\newpage
\section{M\'odulo Diccionario Trie}
%\newcommandx{\RepFuncion}[6][]{
%  \tadOperacion{#1}{#2}{#3}{#4}
%  \tadAxioma{#1(#5)}{#6}
%%%

\begin{Interfaz}
\noindent

  \textbf{Se explica con}: \tadNombre{Diccionario}\\
  \textbf{G\'eneros}: \TipoVariable{dicc\_t}\\
  \textbf{Operaciones}:

	\InterfazFuncion{CrearT}{}{DiccionarioTrie($\alpha$)}
	[$True$]
	{$res \igobs$ vacio}%
	[$\Theta(1)$]
	[Genera un diccionario vacio]

	\InterfazFuncion{Definir}{\Inout{d}{dicc\_t($\alpha$)}, \In{c}{string}, \In{s}{$\alpha$}}{}
	[d $\igobs$ $d_2$]
	{$d$ $\igobs$ definir($c$, $s$, $d_2$ }%
	[$\Theta(long(c))$]
	[Define a c con el significado s]
	[Los elementos se definen por referencia]  

	\InterfazFuncion{Definido?}{\In{d}{dicc\_t($\alpha$), \In{c}{string}}}{bool}
	[$True$]
	{$d$ $\igobs$ def?($c$, $d$)}%
	[$\Theta(long(c)$]
	[Chequea si la clave c est\'a definida en el diccionario]

	\InterfazFuncion{Obtener}{\In{d}{dicc\_t($\alpha$), \In{c}{string}}}{$\alpha$}
	[def?($c$,$d$)]
	{$res$ $\igobs$ significado(c,d)}%
	[$\Theta(long($c$))$]
	[res se devuelve por referencia]\\
	\\
 
\end{Interfaz}

\begin{Representacion}
  
  \Titulo{Representaci\'on de Diccionario Trie}

  \begin{Estructura}{dicc\_t}[str]
    \begin{Tupla}[str]
    \tupItem{ra\'iz}{puntero(Nodo)}
    \end{Tupla}
  \end{Estructura}

  \begin{Estructura}{Nodo}[str]
    \begin{Tupla}[str]
    \tupItem{significado}{puntero($\alpha$)}
    \tupItem{hojas}{arreglo\_estatico de puntero(Nodo)}
    \end{Tupla}
  \end{Estructura}

\noindent\textbf{Elecci\'on de la estructura str}:\\

	La representaci\'on por la cual hemos optado consiste en definir al diccionario
	como un puntero hacia su nodo principal el cual est\'a definido como: los
	elementos que contiene en relaci\'on a la informaci\'on que debe contener hasta
	ese prefijo y un arreglo est\'aico el cual define (en cada sub\'ndice) una
	letra del alfabeto.\\


	\subsubsection{Invariante de Representaci\'on}
	\textbf{Invariante de representaci\'on informal:}
	\begin{enumerate}
	  \item Los nodos dentro del \'arbol no apuntan a su ra\'iz de
	  nuevo.
	  \item Verificar que un mismo nodo no tenga dos padres.
	\end{enumerate}
	
	\textbf{Invariante de representaci\'on formal:}
		
	\Rep[dicc\_t]{$\forall(s, t : Nodo)(contieneNodo(e.raiz, s) \wedge contieneNodo(e.raiz, t))
	\Rightarrow ((hayCamino?(s, t) \wedge \neg hayCamino?(t, s)) \wedge \neg compartenHijos(a, b))\\$}
	
	\RepFuncion{contieneNodo}{puntero(Nodo) /raiz, nodo /Nodo}{boolean}{}
	{raiz, nodo}
	{$\neg (raiz==NULL) \wedge_{L} (*(raiz) = nodo \vee (\exists c : Char)contieneNodo(*(raiz).hojas[c], nodo))$\\}

	\RepFuncion{hayCamino?}{Nodo /a, Nodo /b}{boolean}{$a \neq b$}
 	{a, b}
 	{$(\exists c \in Char)contieneNodo(b.hojas[c], a)\\$}
 	
 	\RepFuncion{compartenHijos}{Nodo /a, Nodo /b}{boolean}{$a \neq b$}
 	{a, b}
 	{$(\exists c \in Char) *(a.hojas[c]) = *(b.hojas[c])\\\\\\$}

	\Abs[dicc\_t]{dicc\_t}{d}{$((\forall s :string) def?(s, d) \leftrightarrow definido?(e,s) \wedge \\
		 ((\forall c:string)  def?(c, d) \rightarrow (obtener(c, d) = obtener(e, c)))$\\\\}

\end{Representacion}

\begin{lstlisting}
	Crear() -> res:dicc\_t{							//O(1)
		res.raiz <- crearNodo()						//O(1)
	}
\end{lstlisting}

\begin{lstlisting}
	Definir(in/out e:estr, in c:string, in s:alfa){				//O(long(c))
		nat i <- 0							
		puntero(Nodo) nodoAux <- e.raiz					//O(1)
		while(i<longitud(c)){						//O(long(c))
			char hoja <- c[i]					//O(1)
			nodoAux <- *(nodoAux).hojas[hoja]			//O(1)

			if(nodoAux == NULL)					//O(1)
				nodoAux <- crearNodo()				//O(1)
			end if
			i <- i+1						
		}end while
		*(*(nodoAux).significado) <- s
	}

COMPLEJIDAD TEMPORAL: O(long(C)), Se recorre la estructura con un ciclo cuya cantidad de 
iteraciones es igual a la cantidad de caracteres de la cadena c y como dentro del cuerpo del ciclo
todas las instrucciones tienen como costo O(1), el costo final del ciclo es O(long(c)).
 
\end{lstlisting}

\begin{lstlisting}
        Definido?(in/out e:estr, in c:string) -> res:bool                       //O(1)
        	nat i <- 0	                                                
		puntero(Nodo) nodoAux <- e.raiz					//O(1)
		res<-true							
		while(i < longitud(c) && res){					//O(long(c))
			hoja <- c[i]						//O(1)
			nodoAux <- *(nodoAux).hojas[hoja]			//O(1)

			if(nodoAux == NULL)					//O(1)
				res <- false					
			end if		

			i <- i+1						
		} end while
		res <- ( (*(nodoAux).significado != NULL) && res)		//O(1)
	}

COMPLEJIDAD TEMPORAL: O(long(C)), Se recorre la estructura con un ciclo cuya cantidad de 
iteraciones es a lo sumo igual a la longitud de la cadena c y como dentro del cuerpo del ciclo
todas las instrucciones tienen como costo O(1), el costo final del ciclo es O(long(c)).
\end{lstlisting}

\begin{lstlisting}

	Obtener(in/out e:estr, in c:string) -> res:alfa{                        //O(1)
		nat i <- 0                                                      
                puntero(Nodo) nodoAux <- e.raiz                                 

                while(i<longitud(c)){                                           //O(long(c))
                         char hoja <- c[i]                                      //O(1)
                         nodoAux <- *(nodoAux).hojas[hoja]                      //O(1)
                         i <- i+1                                                
                }end while							
		res <- *(*nodoAux).significado)					//O(1)
	}

COMPLEJIDAD TEMPORAL: O(long(C)), Se recorre la estructura con un ciclo cuya cantidad de 
iteraciones es igual a la cantidad de caracteres de la cadena c y como dentro del cuerpo del ciclo
todas las instrucciones tienen como costo O(1), el costo final del ciclo es O(long(c)).
\end{lstlisting}

\begin{lstlisting}
        crearNodo() -> res:puntero(Nodo){                                       //O(1)
         
		res.significado <- NULL						//O(1)
		res.hojas <- crearArreglo(256)					//O(1)

		nat i <- 0
		while (i < 256) {						//O(1)
			res.hojas[i] <- NULL					//O(1)
			i <- i + 1						
		}end while
	}

COMPLEJIDAD TEMPORAL: O(1), se crea un nuevo nodo cuyo valor es un puntero a NULL
ya que todavia no se le asigno valor y su arreglo de hijos tiene NULL en todas
las posiciones ya que aun no tiene hijos. Crear y recorrer el arreglo de hijos
cuesta O(1) ya que el tamanio del arreglo es siempre constante.
\end{lstlisting}
